On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory

摘要

This is the first paper to propose a pure event structures model of relaxedmemory. We propose confusion-free event structures over an alphabet with ajustification relation as a model. Executions are modeled by justifiedconfigurations, where every read event has a justifying write event.Justification alone is too weak a criterion, since it allows cycles of the kindthat result in so-called thin-air reads. Acyclic justification forbids suchcycles, but also invalidates event reorderings that result from compileroptimizations and dynamic instruction scheduling. We propose a notionwell-justification, based on a game-like model, which strikes a middle ground.We show that well-justified configurations satisfy the DRF theorem: in anydata-race free program, all well-justified configurations are sequentiallyconsistent. We also show that rely-guarantee reasoning is sound forwell-justified configurations, but not for justified configurations. Forexample, well-justified configurations are type-safe. Well-justification allowsmany, but not all reorderings performed by relaxed memory. In particular, itfails to validate the commutation of independent reads. We discuss variationsthat may address these shortcomings.